k:A sends [tg, e.f(e):B] on l
== ((
e:E. (kind(e) = rcv(l,tg)) 
(valtype(e) 
r B))
== & (
x:Id. vartype(source(l);x) r ds(x)?Top)
== & (
e:E. (kind(e) = k) (loc(e) = source(l)) (valtype(e) r A)))
== c
(e@source(l).
== c
((kind(e) = k) (
isl(f(e))) (
e':E. (kind(e') = rcv(l,tg) & sender(e') = e))
== c
& (e':E.
== c
& ((kind(e') = rcv(l,tg))
== c
& ( ((kind(sender(e')) = k) c (isl(f(sender(e')))) c (val(e') = outl(f(sender(e'))))))
== c
& (e':E.
== c
& ((kind(e') = rcv(l,tg))
== c
& ( (e'':E. (kind(e'') = rcv(l,tg)) (sender(e'') = sender(e')) (e'' = e'))))
clarification:
es-kind-sends-iff(es;k;A;l;tg;B;ds;e.f(e))
== ((
e:es-E(es). (es-kind(es; e) = rcv(l,tg) 
Knd) (es-valtype(es; e) r B))
== & (
x:Id. es-vartype(es; source(l); x) r fpf-cap(ds;IdDeq;x;Top))
== & (
e:es-E(es).
== & ((es-kind(es; e) = k
Knd) (es-loc(es; e) = source(l) Id) (es-valtype(es; e) r A)))
== c
(alle-at(es;source(l);e.(es-kind(es; e) = k Knd)
== c
(isl(f(e)))
== c
(e':es-E(es). (es-kind(es; e') = rcv(l,tg) Knd & es-sender(es; e') = e es-E(es))))
== c
& (e':es-E(es).
== c
& ((es-kind(es; e') = rcv(l,tg) Knd)
== c
& ( ((es-kind(es; es-sender(es; e')) = k Knd)
== c
& ( c (isl(f(es-sender(es; e'))))
== c
& ( c (es-val(es; e') = outl(f(es-sender(es; e'))) B)))
== c
& (e':es-E(es).
== c
& ((es-kind(es; e') = rcv(l,tg) Knd)
== c
& ( (e'':es-E(es).
== c
& ( (es-kind(es; e'') = rcv(l,tg) Knd)
== c
& ( (es-sender(es; e'') = es-sender(es; e') es-E(es))
== c
& ( (e'' = e' es-E(es)))))